Nuprl Lemma : select_append_back
11,40
postcript
pdf
T
:Type,
as
,
bs
:(
T
List),
i
:int_seg(||
as
||; (||
as
|| + ||
bs
||)).
append(
as
;
bs
)[
i
] =
bs
[(
i
- ||
as
||)]
T
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Y
,
append(
as
;
bs
)
,
||
as
||
,
False
,
A
,
prop{i:l}
,
P
Q
,
True
,
A
B
,
P
Q
,
T
,
P
Q
,
P
Q
,
lelt(
i
;
j
;
k
)
,
int_seg(
i
;
j
)
Lemmas
length
wf1
,
int
seg
wf
,
le
wf
,
squash
wf
,
select
wf
,
length
append
,
non
neg
length
,
append
wf
,
select
cons
tl
origin
T:Type, as,bs:(T List), i:int_seg(||as||; (||as|| + ||bs||)).
T T:Type, as,bs:(T List), i:int_seg(||as||; (||as|| + ||bs||)).
T Tx:A. B(x)
A
Q
B
Q
T
Q Q